콘콜릭 테스팅
IT 위키
더 많은 작업
콘콜릭 테스팅(Concolic Testing, Concolic Execution)은 프로그램을 구체적인 입력값으로 실제 실행하면서 동시에 그 실행 경로의 조건을 기호식으로 수집하고, 수집한 조건 일부를 뒤집어 제약 해결기(SMT Solver)로 풀어 다른 경로를 타는 새 입력을 자동으로 만들어 내는 테스트 기법이다.
이름은 구체 실행(Concrete Execution)과 기호 실행(Symbolic Execution)을 합친 말이다. 기호 실행은 입력을 값 대신 기호로 두고 프로그램의 모든 경로 조건을 식으로 풀어 테스트 입력을 찾는 방법이지만, 경로 수가 폭발하고 라이브러리 호출·비선형 연산처럼 풀 수 없는 식이 나오면 진행하지 못한다. 콘콜릭 테스팅은 실제 값으로 실행을 이어 가면서 풀기 어려운 부분은 구체 값으로 바꿔 넣어 이 한계를 줄인다. 그래서 동적 기호 실행(Dynamic Symbolic Execution)이라고도 부른다.
무작위 입력을 쏟아붓는 퍼즈 테스트는 특정 값을 맞혀야만 들어가는 분기(예: if (x == 0x1234abcd))를 거의 통과하지 못한다. 콘콜릭 테스팅은 그 분기 조건을 식으로 풀어 바로 그 값을 만들어 내므로 깊은 경로까지 커버리지를 넓힐 수 있다.
| 단계 | 하는 일 |
|---|---|
| 1. 초기 입력 | 임의의 구체 입력으로 프로그램을 실행한다 |
| 2. 경로 조건 수집 | 실행하면서 지나간 분기마다 조건을 기호식으로 기록한다. 예: x > 0 ∧ y ≠ 5
|
| 3. 조건 부정 | 수집한 조건 중 마지막(또는 선택한) 조건 하나를 뒤집는다. 예: x > 0 ∧ y = 5
|
| 4. 제약 해결 | SMT Solver 로 뒤집은 식을 만족하는 입력을 구한다 |
| 5. 반복 | 새 입력으로 다시 실행해 아직 가지 않은 경로를 탐색한다. 목표 커버리지나 시간 한도까지 되풀이한다 |
| 구분 | 퍼즈 테스트 | 기호 실행 | 콘콜릭 테스팅 |
|---|---|---|---|
| 입력 생성 | 무작위·변이 | 경로 조건을 풀어 생성 | 실제 실행 + 경로 조건 풀이 |
| 실제 실행 | 한다 | 하지 않는다(정적) | 한다 |
| 좁은 조건 분기 | 통과하기 어렵다 | 통과한다 | 통과한다 |
| 약점 | 깊은 경로 도달률이 낮다 | 경로 폭발, 풀 수 없는 식에서 멈춘다 | 경로 폭발은 여전하고 Solver 비용이 크다 |
- 단위 테스트 입력 자동 생성, 화이트박스 테스트 커버리지 향상
- 보안 취약점 탐지 — 퍼저와 결합한 하이브리드 퍼징(Driller 등)
- 도구 : DART, CUTE, KLEE, SAGE(마이크로소프트), CREST, Microsoft Pex/IntelliTest
- 경로 수가 분기 수에 따라 지수적으로 늘어나는 경로 폭발 문제가 남는다
- 암호 해시처럼 역으로 풀 수 없는 조건은 Solver 가 풀지 못한다
- 시스템 호출·외부 환경과 맞물린 부분은 모델링이 필요하다